$\forall$${\it es}$:ES, $i$:Id, ${\it ds}$:$x$:Id fp$\rightarrow$ Type, $I$:(State(${\it ds}$)$\rightarrow\mathbb{P}$).
\\[0ex]@$i$ discrete ${\it ds}$
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. ($\uparrow$first($e$)) $\Rightarrow$ $I$((state when $e$))
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $I$((state when $e$)) $\Rightarrow$ $I$(state after $e$)
\\[0ex]$\Rightarrow$ $\forall$$e$@$i$. $I$((state when $e$))